(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((t1 1)) ((par (T1) ((mkt1 (p1 T1))))))
(declare-datatypes ((t2 1)) ((par (T1) ((mkt2 (p1 T1))))))
(define-fun s1 () (t1 Int) (mkt1 3))
(define-fun s2 () (t2 Int) (mkt2 3))
(define-fun s3 () Int (p1 s1))
(define-fun s4 () Int (p1 s2))
(assert (= s3 s4))
(check-sat)
